(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 58))
(declare-fun v1 () (_ BitVec 69))
(declare-fun v2 () (_ BitVec 80))
(declare-fun v3 () (_ BitVec 91))
(declare-fun v4 () (_ BitVec 94))
(assert (let ((e5(_ bv4352885421546018643 62)))
(let ((e6(_ bv226243851526999446580 68)))
(let ((e7 ((_ rotate_left 16) v1)))
(let ((e8 (bvudiv ((_ sign_extend 22) v1) v3)))
(let ((e9 (ite (= e6 e6) (_ bv1 1) (_ bv0 1))))
(let ((e10 (bvsub ((_ zero_extend 14) v2) v4)))
(let ((e11 (ite (bvule e9 e9) (_ bv1 1) (_ bv0 1))))
(let ((e12 (ite (bvuge v2 ((_ sign_extend 79) e9)) (_ bv1 1) (_ bv0 1))))
(let ((e13 (bvashr ((_ sign_extend 32) e5) e10)))
(let ((e14 (ite (bvsle e10 ((_ zero_extend 26) e6)) (_ bv1 1) (_ bv0 1))))
(let ((e15 ((_ sign_extend 89) e11)))
(let ((e16 (ite (bvuge e10 ((_ zero_extend 93) e12)) (_ bv1 1) (_ bv0 1))))
(let ((e17 (ite (bvuge ((_ zero_extend 1) e6) e7) (_ bv1 1) (_ bv0 1))))
(let ((e18 (bvor ((_ sign_extend 67) e9) e6)))
(let ((e19 (bvnor v2 ((_ zero_extend 22) v0))))
(let ((e20 (bvsle e11 e9)))
(let ((e21 (bvule ((_ sign_extend 57) e16) v0)))
(let ((e22 (= ((_ zero_extend 61) e14) e5)))
(let ((e23 (bvsle ((_ sign_extend 90) e11) e8)))
(let ((e24 (= ((_ zero_extend 93) e14) v4)))
(let ((e25 (bvsle v4 ((_ zero_extend 3) e8))))
(let ((e26 (bvule ((_ zero_extend 67) e12) e18)))
(let ((e27 (bvsgt e13 ((_ zero_extend 93) e12))))
(let ((e28 (= ((_ zero_extend 68) e17) v1)))
(let ((e29 (bvule e15 ((_ sign_extend 10) e19))))
(let ((e30 (bvsle v1 ((_ zero_extend 7) e5))))
(let ((e31 (bvslt e16 e16)))
(let ((e32 (bvslt e19 v2)))
(let ((e33 (bvult ((_ sign_extend 90) e9) e8)))
(let ((e34 (bvsgt e10 ((_ sign_extend 25) e7))))
(let ((e35 (= v4 ((_ zero_extend 93) e16))))
(let ((e36 (bvsgt e7 ((_ zero_extend 1) e6))))
(let ((e37 (bvsge ((_ zero_extend 93) e11) e13)))
(let ((e38 (bvule e18 e18)))
(let ((e39 (bvule e13 ((_ sign_extend 93) e14))))
(let ((e40 (bvslt e9 e17)))
(let ((e41 (bvule e14 e16)))
(let ((e42 (bvult ((_ sign_extend 1) e6) v1)))
(let ((e43 (bvuge ((_ sign_extend 32) e5) e13)))
(let ((e44 (bvsgt ((_ sign_extend 26) e18) v4)))
(let ((e45 (bvugt ((_ sign_extend 67) e12) e6)))
(let ((e46 (bvult e13 ((_ zero_extend 36) v0))))
(let ((e47 (bvslt e8 ((_ zero_extend 90) e17))))
(let ((e48 (bvule ((_ zero_extend 1) e18) v1)))
(let ((e49 (bvule ((_ sign_extend 10) e19) e15)))
(let ((e50 (distinct ((_ zero_extend 79) e9) v2)))
(let ((e51 (bvuge ((_ zero_extend 14) e19) v4)))
(let ((e52 (bvslt e8 ((_ zero_extend 33) v0))))
(let ((e53 (bvule ((_ sign_extend 67) e12) e6)))
(let ((e54 (bvuge e12 e17)))
(let ((e55 (bvuge ((_ sign_extend 3) v3) v4)))
(let ((e56 (=> e26 e21)))
(let ((e57 (xor e41 e50)))
(let ((e58 (=> e42 e46)))
(let ((e59 (ite e31 e43 e31)))
(let ((e60 (ite e55 e24 e37)))
(let ((e61 (and e39 e45)))
(let ((e62 (= e25 e36)))
(let ((e63 (= e59 e48)))
(let ((e64 (xor e22 e63)))
(let ((e65 (and e35 e35)))
(let ((e66 (not e58)))
(let ((e67 (= e54 e34)))
(let ((e68 (xor e57 e23)))
(let ((e69 (and e65 e60)))
(let ((e70 (=> e28 e69)))
(let ((e71 (ite e40 e49 e66)))
(let ((e72 (ite e38 e38 e52)))
(let ((e73 (ite e56 e53 e30)))
(let ((e74 (xor e70 e68)))
(let ((e75 (or e72 e27)))
(let ((e76 (= e44 e33)))
(let ((e77 (and e73 e71)))
(let ((e78 (or e29 e74)))
(let ((e79 (not e64)))
(let ((e80 (not e75)))
(let ((e81 (xor e67 e47)))
(let ((e82 (= e20 e32)))
(let ((e83 (ite e79 e76 e82)))
(let ((e84 (ite e78 e61 e78)))
(let ((e85 (=> e77 e84)))
(let ((e86 (not e81)))
(let ((e87 (xor e85 e86)))
(let ((e88 (ite e83 e51 e83)))
(let ((e89 (ite e87 e62 e80)))
(let ((e90 (and e89 e88)))
(let ((e91 (and e90 (not (= v3 (_ bv0 91))))))
e91
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
